Termination w.r.t. Q proof of /tmp/tmpG7UyhO/cime3.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A¹ → A__A
MARK(k) → A__K
A__A¹ → A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__A¹ → A__B
A__A → A__C
A__A → A__D
MARK(A) → A__A¹
A__H(X, X) → A__K
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__B → A__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__B → A__D

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A¹ → A__A
MARK(k) → A__K
A__A¹ → A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__A¹ → A__B
A__A → A__C
A__A → A__D
MARK(A) → A__A¹
A__H(X, X) → A__K
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__B → A__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__B → A__D

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 12 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(A) → A__A¹
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
MARK(A) → A__A¹
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)

Used ordering: POLO with Polynomial interpretation [25]:

POL(A) = 1
POL(A__A¹) = 0
POL(A__F(x₁)) = 2·x₁
POL(A__G(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(A__H(x₁, x₂)) = x₁ + x₂
POL(A__Z(x₁, x₂)) = x₁ + x₂
POL(MARK(x₁)) = x₁
POL(a) = 0
POL(a__A) = 1
POL(a__a) = 0
POL(a__b) = 0
POL(a__c) = 0
POL(a__d) = 0
POL(a__f(x₁)) = 2·x₁
POL(a__g(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(a__h(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(a__k) = 0
POL(a__z(x₁, x₂)) = x₁ + x₂
POL(b) = 0
POL(c) = 0
POL(d) = 0
POL(e) = 0
POL(f(x₁)) = 2·x₁
POL(g(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(h(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(k) = 0
POL(l) = 0
POL(m) = 0
POL(mark(x₁)) = x₁
POL(z(x₁, x₂)) = x₁ + x₂

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
MARK(f(X)) → A__F(mark(X))
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(f(X)) → A__F(mark(X))
MARK(f(X)) → MARK(X)

The remaining pairs can at least be oriented weakly.

A__F(X) → A__Z(mark(X), X)
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( c ) =

/	0	\
\	0	/

M( a ) =

/	0	\
\	0	/

M( a__b ) =

/	0	\
\	0	/

M( z(x₁, x₂) ) =

/	0	\
\	0	/

/	0	1	\
\	1	0	/

x₁

/	1	0	\
\	0	1	/

x₂

M( a__h(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	1	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( e ) =

/	0	\
\	0	/

M( k ) =

/	1	\
\	0	/

M( mark(x₁) ) =

/	0	\
\	0	/

/	1	0	\
\	0	1	/

x₁

M( d ) =

/	0	\
\	0	/

M( A ) =

/	0	\
\	0	/

M( a__d ) =

/	0	\
\	0	/

M( a__A ) =

/	0	\
\	0	/

M( a__k ) =

/	1	\
\	0	/

M( a__z(x₁, x₂) ) =

/	0	\
\	0	/

/	0	1	\
\	1	0	/

x₁

/	1	0	\
\	0	1	/

x₂

M( m ) =

/	0	\
\	0	/

M( a__c ) =

/	0	\
\	0	/

M( f(x₁) ) =

/	0	\
\	1	/

/	1	1	\
\	1	1	/

x₁

M( l ) =

/	0	\
\	0	/

M( a__g(x₁, ..., x₃) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

/	0	0	\
\	0	0	/

x₃

M( a__f(x₁) ) =

/	0	\
\	1	/

/	1	1	\
\	1	1	/

x₁

M( h(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	1	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( g(x₁, ..., x₃) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

/	0	0	\
\	0	0	/

x₃

M( b ) =

/	0	\
\	0	/

M( a__a ) =

/	0	\
\	0	/

Tuple symbols:

M( A__Z(x₁, x₂) ) =

[

]

x₁

[

]

x₂

M( MARK(x₁) ) =

[

]

x₁

M( A__F(x₁) ) =

[

]

x₁

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

a__a → a__c
a__b → a__c
a__c → l
a__b → a__d
a__k → m
a__k → l
a__c → e
a__a → a__d
a__d → m
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__A → a__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__k → k
a__z(X1, X2) → z(X1, X2)
a__c → c
a__d → d
a__a → a
a__b → b
mark(m) → m
a__A → A
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
MARK(z(X1, X2)) → MARK(X1)
A__F(X) → MARK(X)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK(z(X1, X2)) → MARK(X1)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

A__Z(e, X) → MARK(X)
The graph contains the following edges 2 >= 1
MARK(z(X1, X2)) → MARK(X1)
The graph contains the following edges 1 > 1
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
The graph contains the following edges 1 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A¹

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A__A¹ → A__H(a__f(a__a), a__f(a__b)) at position [] we obtained the following new rules:

A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__c))
A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__A¹ → A__H(a__f(a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__d))
A__A¹ → A__H(a__f(a__c), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__f(a__d))
A__A¹ → A__H(a__f(a__c), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__c))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__A¹ → A__H(a__f(a), a__f(a__b))

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

A__A¹ → A__H(a__f(a__a), a__f(a__c))

The remaining pairs can at least be oriented weakly.

A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__f(a__d))
A__A¹ → A__H(a__f(a__c), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__A¹ → A__H(a__f(a), a__f(a__b))

Used ordering: Combined order from the following AFS and order.
A__A¹ = A__A¹
A__H(x1, x2) = x2
a__z(x1, x2) = x2
mark(x1) = x1
a__a = a__a
a__f(x1) = x1
a__b = a__b
a__d = a__d
A__G(x1, x2, x3) = x1
a__k = a__k
d = d
a__c = a__c
f(x1) = x1
b = b
a = a
l = l
m = m
e = e
A = A
a__A = a__A
c = c
a__h(x1, x2) = a__h
a__g(x1, x2, x3) = a__g
h(x1, x2) = h
g(x1, x2, x3) = g
z(x1, x2) = x2
k = k

Recursive path order with status [2].
Quasi-Precedence:

[a_{_a}, a] > [A_{_A^1}, a_{_b}, a_{_d}, a_{_k}, d, b, A, a_{_A}, a_{_h}, a_{_g}, h, g, k] > [a_{_c}, l, e, c]
[a_{_a}, a] > [A_{_A^1}, a_{_b}, a_{_d}, a_{_k}, d, b, A, a_{_A}, a_{_h}, a_{_g}, h, g, k] > m

Status:

c: multiset
a: multiset
a_{_b}: multiset
a_{_h}: []
e: multiset
A_{_A^1}: multiset
k: multiset
a_{_g}: []
d: multiset
A: multiset
h: []
a_{_d}: multiset
a_{_A}: multiset
a_{_k}: multiset
a_{_c}: multiset
m: multiset
l: multiset
g: []
b: multiset
a_{_a}: multiset

The following usable rules [17] were oriented:

a__a → a__c
a__b → a__c
a__c → l
a__b → a__d
a__k → m
a__k → l
a__c → e
a__a → a__d
a__d → m
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__A → a__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__k → k
a__z(X1, X2) → z(X1, X2)
a__c → c
a__d → d
a__a → a
a__b → b
mark(m) → m
a__A → A
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__A¹ → A__H(a__f(a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A¹ → A__H(a__f(a__c), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__d))

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

A__A¹ → A__H(a__f(a__c), a__f(a__b))

The remaining pairs can at least be oriented weakly.

A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__A¹ → A__H(a__f(a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__d))

Used ordering: Polynomial interpretation [25]:

POL(A) = 1
POL(A__A¹) = 1
POL(A__G(x₁, x₂, x₃)) = x₁
POL(A__H(x₁, x₂)) = x₁
POL(a) = 1
POL(a__A) = 1
POL(a__a) = 1
POL(a__b) = 1
POL(a__c) = 0
POL(a__d) = 1
POL(a__f(x₁)) = x₁
POL(a__g(x₁, x₂, x₃)) = 1
POL(a__h(x₁, x₂)) = 1
POL(a__k) = 0
POL(a__z(x₁, x₂)) = x₂
POL(b) = 1
POL(c) = 0
POL(d) = 1
POL(e) = 0
POL(f(x₁)) = x₁
POL(g(x₁, x₂, x₃)) = 1
POL(h(x₁, x₂)) = 1
POL(k) = 0
POL(l) = 0
POL(m) = 0
POL(mark(x₁)) = x₁
POL(z(x₁, x₂)) = x₂

The following usable rules [17] were oriented:

a__a → a__c
a__b → a__c
a__c → l
a__b → a__d
a__k → m
a__k → l
a__c → e
a__a → a__d
a__d → m
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__A → a__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__k → k
a__z(X1, X2) → z(X1, X2)
a__c → c
a__d → d
a__a → a
a__b → b
mark(m) → m
a__A → A
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__f(b))
A__A¹ → A__H(a__f(a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__d))
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

A__A¹ → A__H(a__f(a__c), a__f(a__b))

The remaining pairs can at least be oriented weakly.

A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__f(a__d))
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__c))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__A¹ → A__H(a__f(a), a__f(a__b))

Used ordering: Polynomial interpretation [25]:

POL(A) = 1
POL(A__A¹) = 1
POL(A__G(x₁, x₂, x₃)) = x₁
POL(A__H(x₁, x₂)) = x₁
POL(a) = 1
POL(a__A) = 1
POL(a__a) = 1
POL(a__b) = 1
POL(a__c) = 0
POL(a__d) = 1
POL(a__f(x₁)) = x₁
POL(a__g(x₁, x₂, x₃)) = 1
POL(a__h(x₁, x₂)) = 1
POL(a__k) = 0
POL(a__z(x₁, x₂)) = x₂
POL(b) = 1
POL(c) = 0
POL(d) = 1
POL(e) = 0
POL(f(x₁)) = x₁
POL(g(x₁, x₂, x₃)) = 1
POL(h(x₁, x₂)) = 1
POL(k) = 0
POL(l) = 0
POL(m) = 0
POL(mark(x₁)) = x₁
POL(z(x₁, x₂)) = x₂

The following usable rules [17] were oriented:

a__a → a__c
a__b → a__c
a__c → l
a__b → a__d
a__k → m
a__k → l
a__c → e
a__a → a__d
a__d → m
mark(a) → a__a
mark(A) → a__A
mark(c) → a__c
mark(b) → a__b
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__A → a__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(e) → e
mark(l) → l
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(d) → a__d
mark(k) → a__k
a__k → k
a__z(X1, X2) → z(X1, X2)
a__c → c
a__d → d
a__a → a
a__b → b
mark(m) → m
a__A → A
a__g(X1, X2, X3) → g(X1, X2, X3)
a__h(X1, X2) → h(X1, X2)
a__f(X) → f(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__A¹ → A__H(a__f(a__a), f(a__b))
A__A¹ → A__H(f(a__a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__c))
A__A¹ → A__H(a__f(a__d), a__f(a__b))
A__A¹ → A__H(a__z(mark(a__a), a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__A¹ → A__H(a__f(a), a__f(a__b))
A__A¹ → A__H(a__f(a__a), a__f(b))
A__G(d, X, X) → A__A¹
A__A¹ → A__H(a__f(a__a), a__z(mark(a__b), a__b))
A__A¹ → A__H(a__f(a__a), a__f(a__d))

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.